
; Copyright (c) 2015 Microsoft Corporation
;; BUG: mpf != fpu [seed=0, num_tests=310]
;; sse2 FPU RM (before) : rm-up 
;; sse2 FPU RM (after) : rm-up 
;; Rounding mode: nearest, ties to even
;; Precision: double (11/53)
;; X = -1.3678820375232716433089308338821865618228912353515625p-148 [- 1656793407106105 -148 N] {- 1656793407106105 -148 (-3.83362e-045)}
;; Y = +1.6458513238706249381948509835638105869293212890625p-295 [+ 2908655781520488 -295 N] {+ 2908655781520488 -295 (2.58548e-089)}
;; Z = +1.8299637333643843373209847413818351924419403076171875p-427 [+ 3737824360310867 -427 N] {+ 3737824360310867 -427 (5.28001e-129)}
;; -1.3678820375232716433089308338821865618228912353515625p-148 [- 1656793407106105 -148 N] x +1.6458513238706249381948509835638105869293212890625p-295 [+ 2908655781520488 -295 N] +1.8299637333643843373209847413818351924419403076171875p-427 [+ 3737824360310867 -427 N] == +1.8299465570760669042016388630145229399204254150390625p-427 [+ 3737747005185201 -427 N]
;; +1.829929380787749249037688059615902602672576904296875p-427

;; mpf : + 3737747005185201 -427
;; mpfd: + 3737747005185201 -427 (5.27996e-129) class: Pos. norm. non-zero
;; hwf : + 3737669650059534 -427 (5.27991e-129) class: Pos. norm. non-zero


(set-logic QF_FP)
(set-info :status unsat)

(define-sort FPN () (_ FloatingPoint 11 53))
(declare-const x FPN)
(declare-const y FPN)
(declare-const z FPN)
(declare-const r FPN)
(declare-const q FPN)
(declare-const mpfx FPN)

(assert (= mpfx (fp.fma roundNearestTiesToEven
		  ((_ to_fp 11 53) roundNearestTiesToEven (- 1.3678820375232716433089308338821865618228912353515625) (- 148))
		  ((_ to_fp 11 53) roundNearestTiesToEven 1.6458513238706249381948509835638105869293212890625 (- 295))
		  ((_ to_fp 11 53) roundNearestTiesToEven 1.8299637333643843373209847413818351924419403076171875 (- 427)))))
;; 	  ((_ to_fp 11 53) roundNearestTiesToEven 1.829929380787749249037688059615902602672576904296875 (- 427))))

(assert (= x ((_ to_fp 11 53) roundNearestTiesToEven (- 1.3678820375232716433089308338821865618228912353515625) (- 148))))
(assert (= y ((_ to_fp 11 53) roundNearestTiesToEven 1.6458513238706249381948509835638105869293212890625 (- 295))))
(assert (= z ((_ to_fp 11 53) roundNearestTiesToEven 1.8299637333643843373209847413818351924419403076171875 (- 427))))
(assert (= r ((_ to_fp 11 53) roundNearestTiesToEven 1.829929380787749249037688059615902602672576904296875 (- 427))))

(assert (= q (fp.fma roundNearestTiesToEven x y z)))

(assert (not (= q r)))

(check-sat)
(check-sat-using smt)

